i:Id, ds:fpf(Id; x.Type), da:fpf(Knd; k.Type), A:ecl(ds; da), snd:msg-spec(ds; da),
upd:update-spec(ds; da).
normal-ds{i:l}
normal-ds(ds)
 normal-da{i:l}
 normal-da(da)
 l_all(ecl-kinds(A);
 l_all(Knd;
 l_all(k.(((isrcv(k))  (i = destination(lnk(k))  Id))  (fpf-dom(Kind-deq; k; da))))
 update-spec-decl(upd; ds)
 msg-spec-loc-decl(snd; i; da)
 ((fpf-dom(id-deq; mkid{ecl:ut2}; ds)))
 R-Feasible{i:l}
 R-Feasible(ecl-machine{ecl:ut2}(i; ds; da; A; snd; upd)) 

latex

Definitions

EqDecider(T), {x:A| B(x)} , l_all(L; T; x.P(x)), prop{i:l}, normal-da{i:l}(da), normal-ds{i:l}(ds), fpf-all(A; eq; f; x,v.P(x;v)), update-spec(ds; da), msg-spec(ds; da), ecl(ds; da), rec(x.A(x)), atom{$n:n}, ecl-mng{i:l}(es; i; ds; da; x; snd; upd), (x  l), ecl-kinds(x), isrcv(k), s = t, destination(l), lnk(k), Kind-deq, Knd, update-spec-decl(upd; ds), msg-spec-loc-decl(snd; i; da), R-Feasible{i:l}(R), ecl-machine{$ecl:ut2}(i; ds; da; A; snd; upd), A, b, fpf-dom(eq; x; f), id-deq, top, fpf(A; a.B(a)), x. t(x), x.A(x), Type, x:A. B(x), Id, mkid{$x:ut2}, t  T, P  Q, x:AB(x), R-realizes{i:l}(R; es.P(es)), P  Q, x:A  B(x)

Lemmas

Id wf, fpf-trivial-subtype-top, id-deq wf, fpf-dom wf, assert wf, not wf, msg-spec-loc-decl wf, update-spec-decl wf, Knd wf, Kind-deq wf, lnk wf, ldst wf, isrcv wf, ecl-kinds wf, l member wf, l all wf2, normal-da wf, normal-ds wf, update-spec wf, msg-spec wf, ecl wf, fpf wf, ecl-realizes